Iof proof for Lemma nat ind tp:
1. P :
{k}
2. P(0)
3.
i:
. P(i - 1) 
P(i)
4. i :
5. 0 < i
6. ((i - 1)
0 ) P(i - 1)
7. i
0
P(i)
by ((Thin (-1))
CollapseTHEN (D (-1)))
C1: .....antecedent..... NILNIL
C1: 5. 0 < i
C1: (i - 1) 0
C2:
C2: 6. P(i - 1)
C2: P(i)
C.